CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THM];

EDIT-STRATEGY-IS: 
DEPTH[2]∨LENGTH[2];

ELAPSED-TIME =1417

NIL 1 2
1 ¬(P(z,x)∧P(x,y));3 4
2 P(G21(x),x);G2
3 ¬G(x,y);THM
4 P(x,z)∧P(z,y)⊃G(x,y);G1